M:MsgA. Sends(M)  k:KndM.da(k)M.stateIdLnk(M.Msg List) 

latex

Definitions	t  T, mlnk(m), x:AB(x), Msg(M), Msg(da), M.Msg, MsgA, IdLnk, Knd, x:A. B(x), M.da(a), M.state, M.sends(k,s,v), a = b, x.A(x), filter(P;l), Sends(M)
Lemmas	filter wf, eq lnk wf, ma-msg wf, ma-send-val wf, IdLnk wf, ma-st wf, ma-da wf, Knd wf, msga wf